Add `btor_aig` option, which uses `model("btor_nomem")` and btor2aiger to generate an aiger file via btor.
Seems to run fine, until it tries to access design_aiger.ywa for trace conversion.

- Add `btor2aig_yw.py` to wrap btor2aiger calls, splitting the symbol map into a
  `.aim` file and building (and approximation of) the `.ywa` file.
- Currently not tracking asserts/assumes in the `.ywa`, and yosys-witness isn't
  the biggest fan of the btor2aiger style of unitialised latches.  As such, the
  latches are declared but the `.yw` output doesn't do anything with them so
  it's incomplete.  But the vcd output seems fine (for `vcd_sim=on|off`).
- Add a try/except to catch property matching with an incomplete property list.
- Add `-x` flag to `write_btor` call since aiw2yw gets confused without them.
- Includes some TODO reminders for me to fix things, but as far as I can tell it
  is working.

Assertions show up in the .btor file as 'bad' statements, assuming btor2aiger maintains the same order this should get us the list of assertions in the order they appear in the .aig file.

Make `-x` flag dependent on `btor_aig on`, and combine with `-c` flag into single `btor_flags` string.

`btor2aiger` tool restarts latch indexing at 0 but aiw2yw expects index to be unique.  Offset latch input number by the total input count to fix this.

Install alongside SBY.
Add env helper to python source.
Fix hardcoded path in `sby_core.py`.

Based on fifo.sby, running both with and without `btor_aig on`, as well as combined with `vcd_sim on` (after an earlier version had issues when using `vcd_sim off`).

Has both pass and fail checks, so should be able to catch any major issues, although it doesn't fully check equivalence.